\documentclass{llncs}

\usepackage{url}
\usepackage{fullpage}
\usepackage{proof}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{xcolor}


\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 --Frank]}}}

\newcommand{\text}[1]{\mbox{#1}}
\newcommand{\wc}{\_}
\newcommand{\mulstep}{ \stackrel{*}{\leadsto}}
\newcommand{\lam}[2]{\lambda #1 . #2}
\newcommand{\evals}[2]{#1 \downarrow #2}

\newcommand{\wm}[0]{\stackrel{\textit{w}}{\to}}
\newcommand{\interp}[1]{[\negthinspace[#1]\negthinspace]}
\newcommand{\symm}[1]{\langle\textit{#1}\rangle}
\newcommand{\rrl}[1]{\textit{r-#1}}
\newcommand{\rrlb}[0]{\textit{r-}\beta}
\newcommand{\trl}[1]{\textit{t-#1}}
\begin{document}
%\pagestyle{empty}
\title{Type Theory a la Russell}
\author{Peng Fu}
\institute{Computer Science, The University of Iowa}
\date{Sep 25, 2012}


\maketitle
\thispagestyle{empty}



\section{Introduction}

\subsection{Lambda Calculus}



From Church, Curry to Howard's notion of construction \cite{dummy}

\subsection{Type Theory}
From Rusell to Today's Calculus of Construction

\subsection{Relation with Verification}

\subsection{Motivations}

\subsection{Overview}





\subsection{}

\subsection{}

\subsection{}

\section{Lambda Encoding}


\section{Type Theory}


\section{Paper Results I}

\subsection{Curry-Howard's Notion of Constructions}

\subsection{Russell's System}
\begin{definition}[Proof Terms]

\

\noindent $ \pi \ ::= \ \mathfrak{a} \ | \ \alpha \ | \ \lambda \alpha:F.\pi \ | \ \pi \pi'\ | \lambda x:T.\pi \ | \ \pi t \ | \ \mathsf{p}^1 \pi \ | \ \mathsf{p}^2 \pi \ | \ \langle \pi_1, \pi_2 \rangle$.

\end{definition}

\noindent Mathfrak letters are used as constants to denote axioms.

\begin{definition}[Pseudo-Terms]

\

\noindent $t \ :: = \ \bot \ | \ x \ |  \ \lambda x.t \ | \ t t'  \ | \ t \supset t' \ | \ \forall x:T.t \ | \ t \wedge t' \ | \ t \vee t' \ | \ \exists x:T.t$



\end{definition}

\noindent Conventions: We use $M$ as metavariable for $t$ when we run out of ways to write pseudo-terms. $\bot$ is used as a constant to denote contradiction.

\begin{definition}[Contexts]

\

\noindent $\mathbf{C} \ :: = \ [] \ |  \ \lambda x.\mathbf{C} \ | \ \mathbf{C} t'  \ | \ t \mathbf{C} \ | \ \mathbf{C} \supset t' \ | \ \ t \supset \mathbf{C} \ | \ \forall x:T.\mathbf{C} \ | \ \mathbf{C} \wedge t' \ | \ \mathbf{C} \vee t' \ | \ t \vee \mathbf{C} \ | \ t \wedge \mathbf{C}  \ | \ \exists x:T.\mathbf{C}$



\end{definition}

\noindent This is a meta notation.
\begin{definition}[Types]

\

\noindent $T \ :: =  \ \iota  \ | \ o \ | \ T \to T'$
\end{definition}

\begin{definition}[Typing]

\

\begin{tabular}{lllll}
\infer{\Delta \vdash x:T}{(x:T) \in \Delta}

& & & &

\infer{\Delta \vdash \lambda x.t : T \to T' }{ \Delta, x:T \vdash t : T'}

\\

\\

\infer{\Delta \vdash t t': T} {\Delta \vdash t: T' \to T & \Delta \vdash t' : T'}

& & & &

\infer{\Delta \vdash \forall x:T.t : o}{ \Delta, x:T \vdash t : o & T \not = o}

\\

\\

\infer{\Delta \vdash t_1 \supset t_2: o}{ \Delta \vdash t_1 : o & \Delta \vdash t_1 : o}

& & & &

\infer{\Delta \vdash \exists x:T.F : o}{ \Delta, x:T \vdash F : o & T \not = o}

\\

\\

\infer{\Delta \vdash t_1 \vee t_2: o}{ \Delta \vdash t_1 : o & \Delta \vdash t_1 : o}

& & & &

\infer{\Delta \vdash  \bot: o}{  }

\\

\\


\end{tabular}
\end{definition}

\noindent Convention: we call $t$ a formula if $\Delta \vdash t:o$, usually written as $F$. We call $t$ a term if $\Delta \vdash t:T$ where $T \not = o$, 
written as $t$.

\begin{definition}[Proofs Annotation]

\

\begin{tabular}{lllll}
\infer{\Delta, \Gamma \vdash \alpha:F} {(\alpha:F) \in \Gamma & \Delta \vdash F:o}

& & & &

\infer{\Delta, \Gamma \vdash \lambda \alpha:F_1.\pi: F_1 \supset F_2 }{ \Delta, \Gamma,\alpha:F_1 \vdash \pi:F_2 & \Delta \vdash F_1 \supset F_2:o}

\\

\\

\infer{\Delta, \Gamma \vdash \lambda x:T.\pi: \forall x:T.F }{\Delta,x:T, \Gamma \vdash \pi:F & \Delta,x:T \vdash F:o & x \notin FV(\Gamma)}

& & & &

\infer{\Delta, \Gamma \vdash \pi_1 \pi_2 : F_2}{\Delta, \Gamma \vdash \pi_1 : F_1 \supset F_2 & \Delta, \Gamma \vdash \pi_2 : F_1}

\\

\\

\infer{\Delta, \Gamma \vdash \pi t : [t/x]F}{\Delta, \Gamma \vdash \pi : \forall x:T.F & \Delta \vdash t : T}

& & & &

\infer{\Delta, \Gamma \vdash \mathsf{p}^1 \pi : F_1}{\Delta, \Gamma \vdash \pi : F_1 \wedge F_2}

\\

\\


\infer{\Delta, \Gamma \vdash \mathsf{p}^2 \pi : F_2}{\Delta, \Gamma \vdash \pi : F_1 \wedge F_2}

& & & &

\infer{\Delta, \Gamma \vdash  \langle \pi_1, \pi_2 \rangle : F_2}{\Delta, \Gamma \vdash \pi_1 : F_1 & \Delta, \Gamma \vdash \pi_2 : F_2}

\\



\end{tabular}
\end{definition}

\begin{definition}[Abrieviations]
\begin{itemize}

\item $t \equiv t' \stackrel{def}{=} (t' \supset t) \wedge (t \supset t')$.

\

\item $ \neg t \stackrel{def}{=} t \supset \bot$

\

\item $ t = t' \stackrel{def}{=} \forall z:T \to o. z t \equiv z t'$

\

\item $ t \not = t' \stackrel{def}{=} \neg (t = t')$

\

\item $ x \  \dot{\in}\ z \stackrel{def}{=} z^{T \to o} x^T$

\

\item $ [x \ | \ F ] \stackrel{def}{=} \lambda x.F$, where $x \in FV(F)$.

\end{itemize}
\end{definition}

\begin{definition}[Frege's comprehensive axiom]
We add one rule to represent Frege's comprehension:

\

\infer{\Delta, \Gamma \vdash  \mathfrak{comp} : \mathbf{C}[(\lambda x.t)t'] \equiv \mathbf{C}[[t'/x]t]}{}


\end{definition}
\noindent The axioms as assumptions idea did not work becuase it can not 
deal forall-intro.

\begin{definition}[Law of Excluded Middle]

\

\infer{\Delta, \Gamma \vdash  e : F \vee \neg F}{}


\end{definition}

\subsection{Tautology}


\begin{theorem}
  $\cdot \vdash \mathfrak{p}^1 : F_1 \wedge F_2 \supset F_1$

$\cdot \vdash \mathfrak{p}^2 : F_1 \wedge F_2 \supset F_2$

\end{theorem}
\subsection{Development of Equality Theory}

\subsection{Development of Peano Postulates}

\begin{theorem}
$ \cdot \vdash \lambda x:T.c: \forall x:T.(\lambda y:T.F)x \equiv [x/y]F$.

\end{theorem}

\begin{proof}

\

\

\infer{\cdot \vdash \lambda x:T.c: \forall x:T.(\lambda y:T.F)x \equiv [x/y]F}{\infer{ x:T \vdash c : (\lambda y:T.F)x \equiv [x/y]F}{}}

\end{proof}


\begin{corollary}
$ \cdot \vdash \lambda x:T.c : \forall x:T.\  ((x \ \dot{\in} \ [\ y:T \ |\ F\ ]) \equiv \ [x/y]F)$.
\end{corollary}

\noindent This is by rewrite the theorem above.



\begin{definition}

\

\begin{itemize}
 \item $\varnothing^{(T \to o) \to o} \stackrel{def}{=} \lambda x:T \to o . (x \not = x) $

\

 \item $[ x^{T \to o} ] \stackrel{def}{=} \lambda y:T\to o . y = x $

\

\item $\overline{x^{T \to o}} \stackrel{def}{=} \lambda y:T. \neg (x^{T \to o} y)$

\

\item $x^{T \to o} \cap y^{T \to o} \stackrel{def}{=} \lambda z:T . x^{T \to o} z \wedge y^{T \to o}z$

\

\item $x^{T \to o} \cup y^{T \to o} \stackrel{def}{=} \lambda z:T . x^{T \to o} z \vee y^{T \to o}z$

\

\item $x \subset y \stackrel{def}{=} \forall z:T.z \ \dot{\in} \ x \supset z \ \dot{\in} \ y$
\end{itemize}
\end{definition}

\begin{definition}

$0 \stackrel{def}{=} [\varnothing]^{((T \to o) \to o) \to o}$

\end{definition}

\begin{definition}
$S \stackrel{def}{=} \lambda x:((T \to o) \to o) \to o.\lambda y:(T \to o) \to o. \exists z:T \to o. (y z \wedge x (y \cap \overline{[z]}))$
\end{definition}

\begin{definition}
$S x \stackrel{def}{=} [ \ y^{(T \to o) \to o} \ | \ \exists z:T \to o. ( z \ \dot{\in} \ y \ \wedge\  (y \cap \overline{[z]})\ \dot{\in}\ x) ] $
\end{definition}

\noindent This is a set-like representation.
\begin{definition}
$Nat \stackrel{def}{=}\lambda x_3:((T \to o) \to o) \to o. \forall x_1 : (((T \to o) \to o) \to o) \to o.$

$ ((x_1 0 \wedge \forall x_2:((T \to o) \to o) \to o . (x_1 x_2 \supset x_1 (S x_2))) \supset x_1 x_3)$


\end{definition}

\begin{definition}
$Nat \stackrel{def}{=}[ \ x_3^{((T \to o) \to o) \to o} \ | \ \forall x_1 . (( 0 \ \dot{\in} \ x_1\wedge \forall x_2 . ( x_2\ \dot{\in} \ x_1\supset (S x_2) \ \dot{\in} \ x_1)) \supset  x_3 \ \dot{\in} \ x_1) \ ]$


\end{definition}
\noindent This is a set-like representation.

\begin{theorem}
$\cdot \vdash \pi : Nat\ 0$ or $ \cdot \vdash \pi : 0 \ \dot{\in} \ Nat$

\end{theorem}

\begin{proof}

\

\infer{
\cdot \vdash \mathfrak{comp}(\lambda x_1. \mathfrak{p}^1) : (\lambda x_3. \forall x_1.((x_1 0 \wedge \forall x_2 . (x_1 x_2 \supset x_1 (S x_2))) \supset x_1 x_3)) 0
}{
\infer{\cdot \vdash \lambda x_1. \mathfrak{p}^1:\forall x_1. ((x_1 0 \wedge x_1 x_2 \supset x_1 (S x_2)) \supset x_1 0)}
{
\infer{\cdot \vdash \mathfrak{p}^1: (x_1 0 \wedge x_1 x_2 \supset x_1 (S x_2)) \supset x_1 0}
{}
}}
\end{proof}

\begin{theorem}
$\cdot \vdash \pi : \forall x. 0 \not = S x$
\end{theorem}

\begin{theorem}

$\cdot \vdash \pi : \forall x. x \ \dot{\in} \ Nat \supset S x\ \dot{\in} \ Nat$
\end{theorem}

\begin{theorem}
$\cdot \vdash \pi :\forall x_1. 0 \ \dot{\in} x_1 \wedge \forall x_2.(x_2 \ \dot{\in} \ x_1 \supset S x_2 \ \dot{\in} \ x_1) \supset Nat \subset x_1 $
\end{theorem}

\begin{theorem}
$\cdot \vdash \pi :\forall x_1. 0 \ \dot{\in} x_1 \wedge \forall x_2.(x_2 \ \dot{\in} \ x_1 \supset S x_2 \ \dot{\in} \ x_1) \supset \forall y( y\ \dot{\in} \ Nat \supset \ y\ \dot{\in} \ x_1) $
\end{theorem}

\begin{theorem}
$\cdot \vdash \pi :\forall x_1. 0 \ \dot{\in} x_1 \wedge \forall x_2.(x_2 \ \dot{\in} \ x_1 \wedge x_2 \ \dot{\in} \ Nat \supset S x_2 \ \dot{\in} \ x_1) \supset \forall y( y\ \dot{\in} \ Nat \supset \ y\ \dot{\in} \ x_1) $


\end{theorem}


\subsection{System F}
To obtain Girard's system F, which intuitively corresponds to higher order propositional logic. We drop the notion of term, and add formula variable 
and quantification over formula variables. And we add two proof terms to handle generalize/instantiation of formula variable.

\begin{definition}[Proof Terms]

\

\noindent $ \pi \ ::= \ \alpha \ | \ \lambda \alpha:F.\pi \ | \ \pi \pi'\ |  \ \pi F \ | \ \Lambda X.\pi$.

\end{definition}

\begin{definition}[Formulas]

\

\noindent $F \ :: = \ X \ | \ F \to F' \ | \ \forall X.F$

\end{definition}

\begin{definition}[Proofs Annotation]

\

\begin{tabular}{lllll}
\infer{\Gamma \vdash \alpha:F} {(\alpha:F) \in \Gamma }

& & & &

\infer{\Gamma \vdash \lambda \alpha:F_1.\pi: F_1 \to F_2 }{  \Gamma,\alpha:F_1 \vdash \pi:F_2 }

\\

\\

\infer{\Gamma \vdash \Lambda X.\pi: \forall X.F }{ \Gamma \vdash \pi:F & X \notin FV(\Gamma)}

& & & &

\infer{\Gamma \vdash \pi_1 \pi_2 : F_2}{\Gamma \vdash \pi_1 : F_1 \to F_2 & \Gamma \vdash \pi_2 : F_1}

\\

\\

\infer{ \Gamma \vdash \pi F' : [F'/X]F}{\Gamma \vdash \pi : \forall X.F }


\end{tabular}
\end{definition}

\noindent Alternatively, one can simply not use the formulaic type system. Adapting the polymorphic type system where $o$ is the only type symbol. The only rule for this polymorphic type system is $x:o$. The notion of well-formed formula and proof annotations remain unchanged. 

\subsection{System $F^{\omega}$}

\noindent To obtain Girard's system $F^{\omega}$, one simply add a type system with types $T \ ::= \ o \ | \ T \to T'$. Others remains unchanged. We can see
now $F^{\omega}$ not only allow quantification over formula, but also quantification over higher order 'formulaic predicate'(a kind of predicate that apply to formula yeilds a formula. etc.). 

\subsection{Martin-L\"of's Type Theory(Dependent Type)}

\noindent It is a bit hard to obtain Martin-L\"of's type theory, since we are going to allow formula to have the ability to quantify over the proofs. 
We adopt a new notion of term  $ t \ ::= \ x \ | \ \lambda x.t \ | \ t t' \ | \ t \pi \ | \ \lambda \alpha.t $. Pseudo-formula $F\ ::= \ t  \ | \ \forall \alpha:F.F$. Types $T \ ::= o \ | \ F \to o \ | \ F \to T$.

\begin{definition}[Formulaic Terms]

\

\begin{tabular}{lllll}
\infer{\Delta, \Gamma \vdash x:T}{(x:T) \in \Delta}

& & & &

\infer{\Delta, \Gamma \vdash \lambda x.t : T \to T' }{ \Delta, x:T, \Gamma \vdash t : T'}

\\

\\

\infer{\Delta, \Gamma \vdash t t': T} {\Delta , \Gamma\vdash t: T' \to T & \Delta, \Gamma \vdash t' : T'}

& & & &

\infer{\Delta , \Gamma\vdash \lambda \alpha.t : F \to T' }{ \Delta,\Gamma, \alpha:F \vdash t : T'}

\\

\\

\infer{\Delta , \Gamma\vdash t \pi: T} {\Delta, \Gamma \vdash t: F \to T & \Gamma \vdash \pi : F}

\\
\end{tabular}
\end{definition}


\begin{definition}[Well-Formed Formulas]

\

\begin{tabular}{lllll}
\infer{\Delta, \Gamma \vdash t : \mathsf{wff}} {\Delta, \Gamma \vdash t : o}

& & & &

\infer{\Delta, \Gamma \vdash \forall \alpha:F.F : \mathsf{wff}}{ \Delta, \Gamma, \alpha:F \vdash F : \mathsf{wff}}

\\


\end{tabular}
\end{definition}

\begin{definition}[Proofs Annotation]

\

\begin{tabular}{lllll}
\infer{\Delta, \Gamma \vdash \alpha:F} {(\alpha:F) \in \Gamma & \Delta,\Gamma \vdash F:\mathsf{wff}}

& & & &

\infer{\Delta, \Gamma \vdash \lambda \alpha:F'.\pi: \forall \alpha:F'.F }{\Delta, \Gamma,\alpha:F' \vdash \pi:F }


\\

\\

\infer{\Delta, \Gamma \vdash \pi \pi' : [\pi'/\alpha]F}{\Delta, \Gamma \vdash \pi : \forall \alpha:F'.F & \Delta,\Gamma \vdash \pi' : F'}


\end{tabular}
\end{definition}

\noindent In order to maintain a degree of independency of terms and proof terms, we have to extend our notion of terms to allow applying them to proof terms. 
\subsection{Church's System}

\subsection{Applications}




\section{Paper Results II}

\section{Implementation}


\section{Conclusions and Future Work}



\bibliographystyle{plain}
\bibliography{comp}

\appendix

\section{Proofs}


\end{document}
